Search for: All records

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the- art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven. 

Si bien una larga historia de datos experimentales muestra que las imágenes térmicas aéreas pueden ser utilizadas para detectar una amplia gama de rasgos arqueológicos tanto superficiales como subsuperficiales, los obstáculos tecnológicos han en gran parte impedido la adopción generalizada de este prometedor método de prospección. Sin embargo, los recientes avances en la sofisticación de las cámaras térmicas, la fiabilidad de los drones comerciales y el creciente poder de los paquetes de software fotogramétricos han puesto al alcance de los arqueólogos la capacidad de recopilar, procesar y analizar imágenes térmicas aéreas. Este artículo ofrece una visión general de la teoría detrás de la aplicación de la termografía aérea en la arqueología, así como una discusión de un conjunto emergente de métodos desarrollados por los autores para llevar a cabo prospecciones remotas. Se resumen las investigaciones realizadas en sitios arqueológicos de Norteamérica, el Mediterráneo y el Cercano Oriente, cuyos resultados ilustran casos en los que la termografía aérea es muy eficaz, así como contextos en los que la cubierta vegetal, la composición del suelo o la profundidad y características específicas de los rasgos arqueológicos presentan desafíos. Destacamos nuevos avances para filtrar el “ruido” causado por la vegetación y métodos para mejorar la visibilidad de los rasgos arqueológicos utilizando imágenes térmicas radiométricas.